YES 1.596
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule List
| ((isPrefixOf :: (Eq b, Eq a) => [(a,b)] -> [(a,b)] -> Bool) :: (Eq a, Eq b) => [(a,b)] -> [(a,b)] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] _ | = | True |
isPrefixOf | _ [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((isPrefixOf :: (Eq a, Eq b) => [(b,a)] -> [(b,a)] -> Bool) :: (Eq b, Eq a) => [(b,a)] -> [(b,a)] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (isPrefixOf :: (Eq b, Eq a) => [(a,b)] -> [(a,b)] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xy2000), Succ(xy4011000)) → new_primPlusNat(xy2000, xy4011000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xy2000), Succ(xy4011000)) → new_primPlusNat(xy2000, xy4011000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xy301100), Succ(xy401100)) → new_primMulNat(xy301100, Succ(xy401100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xy301100), Succ(xy401100)) → new_primMulNat(xy301100, Succ(xy401100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xy30100), Succ(xy40100)) → new_primEqNat(xy30100, xy40100)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xy30100), Succ(xy40100)) → new_primEqNat(xy30100, xy40100)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(app(ty_Either, ba), bb)), bc)) → new_esEs(xy3010, xy4010, ba, bb)
new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(app(ty_Either, bcc), bcd), bce) → new_esEs(xy300, xy400, bcc, bcd)
new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(ty_[], bcb)) → new_esEs3(xy3010, xy4010, bcb)
new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(ty_Maybe, bbd)) → new_esEs0(xy3010, xy4010, bbd)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(app(ty_@2, fh), ga)) → new_esEs1(xy3012, xy4012, fh, ga)
new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(ty_[], bdd), bce) → new_esEs3(xy300, xy400, bdd)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(ty_[], hg)), gh)) → new_esEs3(xy3011, xy4011, hg)
new_esEs0(Just(xy3010), Just(xy4010), app(ty_Maybe, dh)) → new_esEs0(xy3010, xy4010, dh)
new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(ty_Maybe, bbd))) → new_esEs0(xy3010, xy4010, bbd)
new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(ty_Maybe, cf))) → new_esEs0(xy3010, xy4010, cf)
new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(app(ty_Either, df), dg))) → new_esEs(xy3010, xy4010, df, dg)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(ty_Maybe, fg)) → new_esEs0(xy3012, xy4012, fg)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(ty_Maybe, ha)), gh)) → new_esEs0(xy3011, xy4011, ha)
new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(ty_Maybe, bd)), bc)) → new_esEs0(xy3010, xy4010, bd)
new_esEs(Left(xy3010), Left(xy4010), app(ty_Maybe, bd), bc) → new_esEs0(xy3010, xy4010, bd)
new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(app(app(ty_@3, db), dc), dd))) → new_esEs2(xy3010, xy4010, db, dc, dd)
new_esEs(Left(xy3010), Left(xy4010), app(ty_[], cb), bc) → new_esEs3(xy3010, xy4010, cb)
new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), bba) → new_esEs3(xy3011, xy4011, bba)
new_esEs0(Just(xy3010), Just(xy4010), app(app(ty_Either, df), dg)) → new_esEs(xy3010, xy4010, df, dg)
new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(ty_[], bcb))) → new_esEs3(xy3010, xy4010, bcb)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(app(ty_@2, bac), bad), fc, gh) → new_esEs1(xy3010, xy4010, bac, bad)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(app(ty_@2, hb), hc)), gh)) → new_esEs1(xy3011, xy4011, hb, hc)
new_esEs1(@2(xy300, xy301), @2(xy400, xy401), eg, app(app(ty_@2, eh), fa)) → new_esEs1(xy301, xy401, eh, fa)
new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(app(ty_Either, cd), ce))) → new_esEs(xy3010, xy4010, cd, ce)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(app(ty_Either, fd), ff)) → new_esEs(xy3012, xy4012, fd, ff)
new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(app(app(ty_@3, bbg), bbh), bca)) → new_esEs2(xy3010, xy4010, bbg, bbh, bca)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(app(ty_@2, hb), hc), gh) → new_esEs1(xy3011, xy4011, hb, hc)
new_esEs0(Just(xy3010), Just(xy4010), app(ty_[], ef)) → new_esEs3(xy3010, xy4010, ef)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(app(ty_Either, hh), baa)), fc), gh)) → new_esEs(xy3010, xy4010, hh, baa)
new_esEs(Right(xy3010), Right(xy4010), cc, app(app(ty_@2, cg), da)) → new_esEs1(xy3010, xy4010, cg, da)
new_esEs(Right(xy3010), Right(xy4010), cc, app(ty_Maybe, cf)) → new_esEs0(xy3010, xy4010, cf)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(app(ty_Either, fd), ff))) → new_esEs(xy3012, xy4012, fd, ff)
new_esEs0(Just(xy3010), Just(xy4010), app(app(ty_@2, ea), eb)) → new_esEs1(xy3010, xy4010, ea, eb)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(app(app(ty_@3, gb), gc), gd)) → new_esEs2(xy3012, xy4012, gb, gc, gd)
new_esEs(Left(xy3010), Left(xy4010), app(app(ty_Either, ba), bb), bc) → new_esEs(xy3010, xy4010, ba, bb)
new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(app(ty_Either, bbb), bbc)) → new_esEs(xy3010, xy4010, bbb, bbc)
new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(ty_Maybe, bcf), bce) → new_esEs0(xy300, xy400, bcf)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(app(app(ty_@3, bae), baf), bag), fc, gh) → new_esEs2(xy3010, xy4010, bae, baf, bag)
new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(app(app(ty_@3, bg), bh), ca)), bc)) → new_esEs2(xy3010, xy4010, bg, bh, ca)
new_esEs0(Just(xy3010), Just(xy4010), app(app(app(ty_@3, ec), ed), ee)) → new_esEs2(xy3010, xy4010, ec, ed, ee)
new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(ty_Maybe, dh))) → new_esEs0(xy3010, xy4010, dh)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(app(ty_Either, gf), gg)), gh)) → new_esEs(xy3011, xy4011, gf, gg)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(app(ty_Either, hh), baa), fc, gh) → new_esEs(xy3010, xy4010, hh, baa)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(ty_[], ge))) → new_esEs3(xy3012, xy4012, ge)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(ty_[], hg), gh) → new_esEs3(xy3011, xy4011, hg)
new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(app(ty_@2, bbe), bbf))) → new_esEs1(xy3010, xy4010, bbe, bbf)
new_esEs(Left(xy3010), Left(xy4010), app(app(ty_@2, be), bf), bc) → new_esEs1(xy3010, xy4010, be, bf)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(ty_[], bah)), fc), gh)) → new_esEs3(xy3010, xy4010, bah)
new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], bba)) → new_esEs3(xy3011, xy4011, bba)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(app(app(ty_@3, gb), gc), gd))) → new_esEs2(xy3012, xy4012, gb, gc, gd)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(ty_Maybe, ha), gh) → new_esEs0(xy3011, xy4011, ha)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(ty_Maybe, fg))) → new_esEs0(xy3012, xy4012, fg)
new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(app(app(ty_@3, bbg), bbh), bca))) → new_esEs2(xy3010, xy4010, bbg, bbh, bca)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(app(app(ty_@3, bae), baf), bag)), fc), gh)) → new_esEs2(xy3010, xy4010, bae, baf, bag)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(ty_Maybe, bab), fc, gh) → new_esEs0(xy3010, xy4010, bab)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(app(ty_Either, gf), gg), gh) → new_esEs(xy3011, xy4011, gf, gg)
new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(app(ty_@2, cg), da))) → new_esEs1(xy3010, xy4010, cg, da)
new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(app(ty_Either, bbb), bbc))) → new_esEs(xy3010, xy4010, bbb, bbc)
new_esEs(Right(xy3010), Right(xy4010), cc, app(app(ty_Either, cd), ce)) → new_esEs(xy3010, xy4010, cd, ce)
new_esEs(Right(xy3010), Right(xy4010), cc, app(ty_[], de)) → new_esEs3(xy3010, xy4010, de)
new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(app(ty_@2, bbe), bbf)) → new_esEs1(xy3010, xy4010, bbe, bbf)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(ty_[], ge)) → new_esEs3(xy3012, xy4012, ge)
new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(app(ty_@2, ea), eb))) → new_esEs1(xy3010, xy4010, ea, eb)
new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(ty_[], cb)), bc)) → new_esEs3(xy3010, xy4010, cb)
new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(ty_[], de))) → new_esEs3(xy3010, xy4010, de)
new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(app(app(ty_@3, ec), ed), ee))) → new_esEs2(xy3010, xy4010, ec, ed, ee)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(app(app(ty_@3, hd), he), hf), gh) → new_esEs2(xy3011, xy4011, hd, he, hf)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(app(ty_@2, bac), bad)), fc), gh)) → new_esEs1(xy3010, xy4010, bac, bad)
new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(app(ty_@2, bcg), bch), bce) → new_esEs1(xy300, xy400, bcg, bch)
new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(ty_[], bah), fc, gh) → new_esEs3(xy3010, xy4010, bah)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(app(app(ty_@3, hd), he), hf)), gh)) → new_esEs2(xy3011, xy4011, hd, he, hf)
new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(app(ty_@2, be), bf)), bc)) → new_esEs1(xy3010, xy4010, be, bf)
new_esEs(Right(xy3010), Right(xy4010), cc, app(app(app(ty_@3, db), dc), dd)) → new_esEs2(xy3010, xy4010, db, dc, dd)
new_esEs(Left(xy3010), Left(xy4010), app(app(app(ty_@3, bg), bh), ca), bc) → new_esEs2(xy3010, xy4010, bg, bh, ca)
new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(ty_[], ef))) → new_esEs3(xy3010, xy4010, ef)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(app(ty_@2, fh), ga))) → new_esEs1(xy3012, xy4012, fh, ga)
new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(ty_Maybe, bab)), fc), gh)) → new_esEs0(xy3010, xy4010, bab)
new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(app(app(ty_@3, bda), bdb), bdc), bce) → new_esEs2(xy300, xy400, bda, bdb, bdc)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(app(ty_@2, bbe), bbf)) → new_esEs1(xy3010, xy4010, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xy3010), Just(xy4010), app(app(ty_@2, ea), eb)) → new_esEs1(xy3010, xy4010, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xy3010), Just(xy4010), app(ty_[], ef)) → new_esEs3(xy3010, xy4010, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(app(app(ty_@3, bbg), bbh), bca)) → new_esEs2(xy3010, xy4010, bbg, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xy3010), Just(xy4010), app(app(app(ty_@3, ec), ed), ee)) → new_esEs2(xy3010, xy4010, ec, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(ty_Maybe, bbd)) → new_esEs0(xy3010, xy4010, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(app(ty_Either, bbb), bbc)) → new_esEs(xy3010, xy4010, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xy3010), Just(xy4010), app(ty_Maybe, dh)) → new_esEs0(xy3010, xy4010, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xy3010), Just(xy4010), app(app(ty_Either, df), dg)) → new_esEs(xy3010, xy4010, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Right(xy3010), Right(xy4010), cc, app(app(ty_@2, cg), da)) → new_esEs1(xy3010, xy4010, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Left(xy3010), Left(xy4010), app(app(ty_@2, be), bf), bc) → new_esEs1(xy3010, xy4010, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Left(xy3010), Left(xy4010), app(ty_[], cb), bc) → new_esEs3(xy3010, xy4010, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(xy3010), Right(xy4010), cc, app(ty_[], de)) → new_esEs3(xy3010, xy4010, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Left(xy3010), Left(xy4010), app(app(app(ty_@3, bg), bh), ca), bc) → new_esEs2(xy3010, xy4010, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Right(xy3010), Right(xy4010), cc, app(app(app(ty_@3, db), dc), dd)) → new_esEs2(xy3010, xy4010, db, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(Left(xy3010), Left(xy4010), app(ty_Maybe, bd), bc) → new_esEs0(xy3010, xy4010, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(xy3010), Right(xy4010), cc, app(ty_Maybe, cf)) → new_esEs0(xy3010, xy4010, cf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Left(xy3010), Left(xy4010), app(app(ty_Either, ba), bb), bc) → new_esEs(xy3010, xy4010, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Right(xy3010), Right(xy4010), cc, app(app(ty_Either, cd), ce)) → new_esEs(xy3010, xy4010, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, xy301), @2(xy400, xy401), eg, app(app(ty_@2, eh), fa)) → new_esEs1(xy301, xy401, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(app(ty_@2, hb), hc)), gh)) → new_esEs1(xy3011, xy4011, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(app(ty_@2, bbe), bbf))) → new_esEs1(xy3010, xy4010, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(app(ty_@2, cg), da))) → new_esEs1(xy3010, xy4010, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(app(ty_@2, ea), eb))) → new_esEs1(xy3010, xy4010, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(app(ty_@2, bcg), bch), bce) → new_esEs1(xy300, xy400, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(app(ty_@2, bac), bad)), fc), gh)) → new_esEs1(xy3010, xy4010, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(app(ty_@2, be), bf)), bc)) → new_esEs1(xy3010, xy4010, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(app(ty_@2, fh), ga))) → new_esEs1(xy3012, xy4012, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(app(ty_@2, fh), ga)) → new_esEs1(xy3012, xy4012, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(app(ty_@2, bac), bad), fc, gh) → new_esEs1(xy3010, xy4010, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(app(ty_@2, hb), hc), gh) → new_esEs1(xy3011, xy4011, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), app(ty_[], bcb)) → new_esEs3(xy3010, xy4010, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(xy3010, xy3011), :(xy4010, xy4011), bba) → new_esEs3(xy3011, xy4011, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(ty_[], bdd), bce) → new_esEs3(xy300, xy400, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(ty_[], hg)), gh)) → new_esEs3(xy3011, xy4011, hg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(ty_[], bcb))) → new_esEs3(xy3010, xy4010, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(ty_[], ge))) → new_esEs3(xy3012, xy4012, ge)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(ty_[], bah)), fc), gh)) → new_esEs3(xy3010, xy4010, bah)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], bba)) → new_esEs3(xy3011, xy4011, bba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(ty_[], cb)), bc)) → new_esEs3(xy3010, xy4010, cb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(ty_[], de))) → new_esEs3(xy3010, xy4010, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(ty_[], ef))) → new_esEs3(xy3010, xy4010, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(ty_[], hg), gh) → new_esEs3(xy3011, xy4011, hg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(ty_[], ge)) → new_esEs3(xy3012, xy4012, ge)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(ty_[], bah), fc, gh) → new_esEs3(xy3010, xy4010, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(app(app(ty_@3, db), dc), dd))) → new_esEs2(xy3010, xy4010, db, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(app(app(ty_@3, bg), bh), ca)), bc)) → new_esEs2(xy3010, xy4010, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(app(app(ty_@3, gb), gc), gd))) → new_esEs2(xy3012, xy4012, gb, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(app(app(ty_@3, bbg), bbh), bca))) → new_esEs2(xy3010, xy4010, bbg, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(app(app(ty_@3, bae), baf), bag)), fc), gh)) → new_esEs2(xy3010, xy4010, bae, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(app(app(ty_@3, ec), ed), ee))) → new_esEs2(xy3010, xy4010, ec, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(app(app(ty_@3, hd), he), hf)), gh)) → new_esEs2(xy3011, xy4011, hd, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(app(app(ty_@3, bda), bdb), bdc), bce) → new_esEs2(xy300, xy400, bda, bdb, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(ty_Maybe, bbd))) → new_esEs0(xy3010, xy4010, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(ty_Maybe, cf))) → new_esEs0(xy3010, xy4010, cf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(ty_Maybe, bd)), bc)) → new_esEs0(xy3010, xy4010, bd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(ty_Maybe, ha)), gh)) → new_esEs0(xy3011, xy4011, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(ty_Maybe, bcf), bce) → new_esEs0(xy300, xy400, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(ty_Maybe, dh))) → new_esEs0(xy3010, xy4010, dh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(ty_Maybe, fg))) → new_esEs0(xy3012, xy4012, fg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(ty_Maybe, bab)), fc), gh)) → new_esEs0(xy3010, xy4010, bab)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, Left(xy3010)), @2(xy400, Left(xy4010)), eg, app(app(ty_Either, app(app(ty_Either, ba), bb)), bc)) → new_esEs(xy3010, xy4010, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, xy301), @2(xy400, xy401), app(app(ty_Either, bcc), bcd), bce) → new_esEs(xy300, xy400, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy300, Just(xy3010)), @2(xy400, Just(xy4010)), eg, app(ty_Maybe, app(app(ty_Either, df), dg))) → new_esEs(xy3010, xy4010, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, Right(xy3010)), @2(xy400, Right(xy4010)), eg, app(app(ty_Either, cc), app(app(ty_Either, cd), ce))) → new_esEs(xy3010, xy4010, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, app(app(ty_Either, hh), baa)), fc), gh)) → new_esEs(xy3010, xy4010, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), fc), app(app(ty_Either, fd), ff))) → new_esEs(xy3012, xy4012, fd, ff)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, @3(xy3010, xy3011, xy3012)), @2(xy400, @3(xy4010, xy4011, xy4012)), eg, app(app(app(ty_@3, fb), app(app(ty_Either, gf), gg)), gh)) → new_esEs(xy3011, xy4011, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, :(xy3010, xy3011)), @2(xy400, :(xy4010, xy4011)), eg, app(ty_[], app(app(ty_Either, bbb), bbc))) → new_esEs(xy3010, xy4010, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(app(app(ty_@3, gb), gc), gd)) → new_esEs2(xy3012, xy4012, gb, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(app(app(ty_@3, bae), baf), bag), fc, gh) → new_esEs2(xy3010, xy4010, bae, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(app(app(ty_@3, hd), he), hf), gh) → new_esEs2(xy3011, xy4011, hd, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(ty_Maybe, fg)) → new_esEs0(xy3012, xy4012, fg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(ty_Maybe, ha), gh) → new_esEs0(xy3011, xy4011, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(ty_Maybe, bab), fc, gh) → new_esEs0(xy3010, xy4010, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, fc, app(app(ty_Either, fd), ff)) → new_esEs(xy3012, xy4012, fd, ff)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), app(app(ty_Either, hh), baa), fc, gh) → new_esEs(xy3010, xy4010, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(xy3010, xy3011, xy3012), @3(xy4010, xy4011, xy4012), fb, app(app(ty_Either, gf), gg), gh) → new_esEs(xy3011, xy4011, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba, bb) → new_isPrefixOf(xy31, xy41, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba, bb) → new_isPrefixOf(xy31, xy41, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4